E:Type, eq:EqDecider(E), prd:(E(?E)), info:(E((:Id  Id) + (:(:IdLnk  E)  Id))),
oax:EOrderAxioms(E; prd; info), T:(IdIdType), w, a:(x:Ide:ET(loc(e),x)),
sax:(e:E. ((first(e)))  (x:Id. w(x,e) = a(x,pred(e))  T(loc(e),x))), V:(KndIdType),
v:(e:EV(kind(e),loc(e))).
mk-eval(E;eq;prd;info;oax;T;w;a;sax;V;v)  EventsWithValues 

latex

Definitions	x:A. B(x), P  Q, t  T, , EventsWithValues, mk-eval(E;eq;prd;info;oax;T;w;a;sax;V;v), Top, EOrderAxioms(E; pred?; info), P & Q, A c B
Lemmas	kind wf, loc wf, Id wf, Knd wf, not wf, assert wf, first wf, EOrderAxioms wf, IdLnk wf, unit wf, deq wf, top wf, pred wf, subtype rel self